Inference at * 1 2 
Iof proof for Lemma p-fun-exp-add1-sq:

.....upcase..... NILNIL

1. A : Type
2. f : A(A + Top)
3. x : A
4. isl(f(x))
5. n : 
6. 0 < n
7. (primrec(n - 1;f o p-id()  ;i,g. f o g  )(x))
7. ~
7. (primrec(n - 1;p-id();i,g. f o g  )(outl(f(x))))
  (primrec(n;f o p-id()  ;i,g. f o g  )(x)) ~ (primrec(n;p-id();i,g. f o g  )(outl(f(x)))) 

latex

 by (RecUnfold `primrec` 0) 
CollapseTHEN (((if (0) =0 then SplitOnConclITE else SplitOnHypITE (0
C))) 
CollapseTHENA (Auto)) 

latex

C1: .....truecase..... NILNIL

C1: 8. n = 0
C1:   (f o p-id()  (x)) ~ (p-id()(outl(f(x))))
C2: .....falsecase..... NILNIL

C2: 8. (n = 0)
C2:   ((i,g. f o g  )((n - 1),primrec(n - 1;f o p-id()  ;i,g. f o g  ),x))
C2:   ~
C2:   ((i,g. f o g  )((n - 1),primrec(n - 1;p-id();i,g. f o g  ),outl(f(x))))
C.

Definitions	left + right, Unit, P  Q, P & Q, x:A  B(x), P  Q, x:AB(x), (i = j), #$n, , b, , s = t, , A, t  T, b, x:A. B(x)
Lemmas	eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, bool wf, bnot wf, not wf, assert wf